$\forall$$T$:Type, $P$:($T$$\rightarrow\mathbb{B}$), ${\it T'}$:Type, $f$:(\{$x$:$T$$\mid$ $\uparrow$($P$($x$))\} $\rightarrow$${\it T'}$), $L$:($T$ List).
\\[0ex]mapfilter($f$; $P$; $L$) $\in$ (${\it T'}$ List)